wpfacts: interval rule results are not widened, and a counter write on a leaving path keeps the narrowed reads (R1 range tightening) - #14416

The two range-analysis follow-ups of PR-C3 (#14402, FOLLOWUPS "ranges: sum widening" and "ranges: counter written in a leaving branch"). Both are wpfacts-only; codegen is unchanged and obeys the tighter facts (more field read calls in the board's floor).

What changes

• (a) Sum widening: the step that overshoots. solve::grow_range widened every node after WIDEN_STEPS (3) growths, the result of an interval rule (Cons::Range) included. A sum grows once for every growth of either operand, so r * 16 + f passed 3 growths while its operands were still climbing and jumped to the ladder's rungs (127, then 255), although its operands end at [0, 7]. The widening that terminates a loop belongs to the loop counter, a copy target, and the loop test clips it back (gen::narrow). Now a rule result takes the plain join of its rule's evaluations (solve::grow_rule_range): the rule over its operands' final intervals. Copy targets widen as before.

  • Termination: rule results form no cycle among themselves. A rule's operands exist before its result node is ruled, and a result has one rule. So every cycle passes a copy target, which widens, and a result grows at most once per operand growth. Past WIDEN_LIMIT growths a result still climbs the ladder, a backstop for any cycle the argument missed (never ⊤ from the step count alone).
  • Probe (C3's): at(r*16) [0,112] (unchanged), at(r*16+f) [0,255] → [0,119], at(r+f) [0,127] → [0,14], the down-counting form [0,119] (unchanged).

• (b) A counter write in a branch that leaves. gen/narrow.rs ended a narrowing's start reads at the first write in the program text. It now ends them where the write can reach. After a branch of an if that always leaves (always_exits), each narrowing's written is restored to its value before the branch (Gen::narrow_snapshot / narrow_leave), when every way out of the branch lands outside the narrowed code:

  • an unlabeled break/continue with no loop or switch between the if and the narrowing (Gen::jumps, counted at loop bodies and switch cases): it lands at the narrowed loop's update, which reads the end node, or past the guarded code;
  • a return/throw, and any exception, with no try between them (Gen::tries): no catch or finally of the narrowed code runs after it;
  • no labeled jump anywhere in the branch (jumps_leave; where it lands is not followed).

  The write still edges into the end node and the local, so the update and every read the jump reaches see it. This is a forward may-write analysis over the structured control flow, with the abrupt edges resolved by their targets, not the text order. for (let sq = 0; sq < 128; sq++) { if ((sq & 0x88) !== 0) { sq += 7; continue; } … this.at(sq) } reads [0,127] instead of [0,255].

• Switches: PERRY_FACTS_EXACT_RULES=0 (rule results widen like any node again) and PERRY_FACTS_LEAVING_WRITES=0 (first textual write ends the reads again). Both off is main exactly. Both are compile-cache inputs (compile_env.rs, test range_tightening_switches_are_cache_inputs).

• Sabotage: PERRY_FACTS_SABOTAGE=exactrule (a sum's interval is the hull of its operands, not their sum) and leavingwrite (every branch's writes are dropped from the reads after it, also a branch that falls through). S0 fixtures range-sum-negative.ts (r*16+f on a 116-element board: the false [0,112] is in the floor, real keys reach 119) and leaving-write-negative.ts (a q += 20 that falls through to the read, 16-element board). Both are caught by the element tier's witness at the key ("array rep").

• Tests: perry-wpfacts tests/range_tightening.rs, 5 tests: the probe shapes in the floor; the else branch that leaves; both switches off give the widened intervals back. The negative controls stay wide: a write that falls through; a break out of a switch that lands before the read; a continue whose finally reads; a labeled continue; a sum whose hull is past the floor. The two sabotage arms claim a read in the floor that is not. Parity fixture tests/parity/language/array/test_range_tightening.ts: the in-floor shapes, the leaving continue/else/return/break/guarded return, and the negative controls (falls through, switch, try/finally, try/catch with throw, labeled, a write in an inner loop, a guard over a loop that writes), on a 128- and a 64-element board.

• Dump: unchanged. # field_read_call … key= in_floor= shows the verdicts.

Chess sites (PERRY_FACTS_DUMP, 35 field read calls on Chess.board = arr<f64,128,dense>)

In the floor: 32 of 35 (off: 27, as C3). Newly in the floor are the five sites C3 named: evaluate:369 passed pawn at(r*16+f) [0,119], evaluate:342/354 at(square) [0,127], and generatePseudo:590 at(from) and :741 at(square) [0,127]. Still out, as the design expects (finding 13): set:464 [-128,255], make:652 at(captureSquare) and generatePseudo:599 at(to + direction) [-16,143].

Results (qb9, instructions:u)

Build 631a293855 = this branch with origin/main 85ee3399a3 merged (C3, N3 #14406, N4 #14407). On vs both switches off on the same binary, two runs each. The runs were identical to 0.1 M and the checksums equal in every run.

Re-measured on qb10 (a different CPU; its own table, build 93bb48b2f2, the head's code, on vs off on the same binary, two identical runs):

The branch head 5bdd2e4d36 merges origin/main dd48c42e80 (clean). On qb10 it gives the same chess counts: search 25 770.8 / 27 377.4, perft 610.1 / 622.1, evaluate 1 881.9 / 2 516.9, legal 976.8 / 989.3. It also has perry-wpfacts 2295 passed / 0 failed, S0 rc 0 and 32 of 35 calls in the floor.

The arms are not additive on evaluate: the passed-pawn loop sits inside the square loop and reads square >> 4 and square & 7. C3's per-read estimate (−10% evaluate, −1.9% search) was low. The design priced an in-floor read at 8 instructions saved, but the in-floor form also drops the ?? select and the cold arm. Perft and legal gain only from generatePseudo:590 (the leaving write). Before the merge of N3/N4 (build 1231ef360a on main 821bf58): search 29 151.6 / 30 760.9 (−5.23%), perft 701.4 / 710.5 (−1.28%), evaluate 2 174.9 / 2 847.7 (−23.63%), legal 1 064.0 / 1 073.4 (−0.88%). That off arm equals C3's measured main.

Size (every executable section; on vs off)

Supabase's perry_js_text grows 1 664 B. That is below the accepted 0.001% and not attributed per symbol: tighter intervals make more int32 locals, whose code can be larger or smaller.

Departures and what is not done

• The fix for (a) is at the rule result, not "widen each counter, then add". It amounts to that: the counter (a copy target) still widens and is clipped by its test, and the sum then adds the clipped intervals. The sum only loses its own widening. A copy target that copies a growing sum (const k = r*16+f; at(k)) still widens on its own step count (at most to the rung above the hull). A single-definition const needs no widening either, but that needs a node flag and its own census (FOLLOWUPS).
• (b) is conservative where control flow is not followed: a labeled break/continue, a jump out of a nested switch or loop, and any try between the if and the narrowing keep the textual rule. An else branch still starts from the then branch's state (sound, not tight).
• The exactrule sabotage is a wrong transfer (a sum is its operands' hull), not a broken widening. The first version froze each rule result at its first interval, which depends on the solve order. In the compile driver the first evaluation was already final, so no false claim was made: the unit test's solve made it, S0's compile did not.
• The S0 fixtures read through a b1 call whose key is a local, not a loop counter. With a key computed from loop counters (r*16+f, a for counter), codegen routes the call to the index method clone (at$idx_u31_2$i32, lower_call/index_split.rs) instead of b1's in-floor read. The sabotaged claim is made (the dump shows in_floor=1), but nothing consumes it, so no witness fires. The fixtures use a const ep = this.ep key (as C3's arrb1) and a guard-narrowed local. The routing is codegen's, outside this lane: FOLLOWUPS "[b1 vs the index method clone]".
• Mac: not built (disk). Gates, suites and the first table ran on qb9; the second table, the rel3 build and the final S0 ran on qb10.

Summary by CodeRabbit

• Improvements
  • Whole-program analysis now preserves tighter value ranges in more cases, including some calculations and branches that exit before a later read. This can improve analysis of indexed array access.
  • Added environment-variable controls to disable these range-tightening behaviors when needed. Changes to these settings are included in compile cache keys.
• Tests
  • Added coverage for tighter ranges, control-flow scenarios, configuration switches, and indexed array access.